#include "base/aig.h"
#include "minisat-2.2/Solver.h"
#include "cktsat/cktcover.h"
#include "cktsat/satsolver.h"
#include "cktsat/msatsolver.h"
#include "lut.h"
#include "rewrite/synit.h"
#include "cktsat/fraig.h"
#include <fstream>
#include <tr1/unordered_map>
#include <algorithm>

using Minisat::lbool;
using Minisat::l_True;
using Minisat::l_False;
using std::vector;

using std::cout;
using std::endl;

//#define NO_TRI_STATE

typedef Minisat::vec< Minisat::Lit > cls_t;

int 		Parameter::SIM_SIZE 			= 20;	// pat  factor 
int 		Parameter::SIM_GOOD_SIZE	= 10; // pat  factor 
int 		Parameter::SAT_PAT_OUT_SIZE= 10; // pat  factor 
int 		Parameter::P_SEL_SAT_OUT   = 2;  // rand factor
double   Parameter::CAND_SCORE		= 10.0;//cand1 factor

int 		Parameter::CAND_UBOUND     = 15; // cand1 factor
int 		Parameter::CAND_LBOUND     = 5;  // cand1 factor

int 		Parameter::PAT_SIM_CONF 	= 100;  //fix factor
int 		Parameter::PAT_SAT_CONF 	= 10000;//fix factor

int 		Parameter::SYN_BY_SAT_CONFLICT=0;
int 		Parameter::FIX_ALL 			= 1;

double   Parameter::PUSH_TO_INPUT_FACTOR=1.2;//rand factor
double   Parameter::PUSH_TO_OUTPUT_FACTOR=1;//rand factor
double 	Parameter::FILTER_FACTOR 	= 2.0;   //rand factor
double 	Parameter::REFINE_FACTOR1  = 1.5;   //cand2 factor
double   Parameter::REFINE_FACTOR2  = 1.5;   //cand2 factor

template<class T1,class T> inline void bound( T1 & x , T high , T low )
{
	if( x > high ) x = high;
	if( x < low  ) x = low;
}
void Parameter::change_cand1( int up )
{
	if( rand() % 2 ) return ;
	bound( Parameter::CAND_UBOUND += up * 3 , 100 , 1 );
	bound( Parameter::CAND_LBOUND += up * 2 , 100 , 1 );
	bound( Parameter::CAND_SCORE  += up * 1 , 20.0 , 1.2 );
}
void Parameter::change_cand2( int up )
{
	if( rand() % 2 ) return;
	bound( Parameter::REFINE_FACTOR1 += up * 0.3 , 7.0 , 1.0 );
	bound( Parameter::REFINE_FACTOR2 += up * 0.5 , 10.0 , 1.0 );
}
void Parameter::change_pat( int up )
{
	if( rand() % 2 ) return;
	bound( Parameter::SIM_SIZE += up * 10 , 1000 , 5 );
	bound( Parameter::SIM_GOOD_SIZE += up * 10 , 1000 , 1 );
	bound( Parameter::SAT_PAT_OUT_SIZE += up * 10 , 1000 , 1 );
}
void Parameter::change()
{
	if( rand() % 2 ) return;
	int up = (rand()&1)?1:(-1);
	bound( Parameter::PUSH_TO_INPUT_FACTOR += up*0.2 , 0.2 , 3.0 );
//	up = (rand()&1)?1:-1;bound( Parameter::PUSH_TO_OUTPUT_FACTOR += up*0.05 , 0.5 , 1.2 );
	up = (rand()&1)?1:-1;
	bound( Parameter::FILTER_FACTOR += up*0.3 , 0.2 , 3.0 );
}
struct Triple 
{
   unsigned dat[3];
   Triple( unsigned d0 , unsigned d1 , unsigned d2 ){ dat[0]=d0 , dat[1]=d1 , dat[2]=d2; }
   Triple(){}
};
struct GetVar
{
   unsigned _base , _diff;
   void init( unsigned b , unsigned nv ){ _base = b , _diff = nv-b;}
   unsigned operator()( unsigned i , unsigned j )
   {
      if( j < _base )return j ;
      return i*_diff + j;
   }
   Lit operator()( unsigned i , Lit x )
   {
      if( x.var() < _base ) return x;
      return Lit( i * _diff + x.var() , x.sign() );
   }
};
struct MuxCktLit // use for phase 2 refine candidate 
{
   Lit * selection; 
   Lit * rewire;
   Lit * lits;
   MuxCktLit( unsigned candsize , unsigned designsize )
   { 
      selection = new Lit[ candsize ];
      rewire    = new Lit[ candsize ];
      lits      = new Lit[ designsize ];
   }
   ~MuxCktLit(){
      delete [] selection ;
      delete [] rewire ;
      delete [] lits;
   }
};
struct ECODB
{
   vector<uint8_t> cls[1<<(1<<4)];
   uint8_t         inv[1<<(1<<4)];

   ECODB( const char * f )
   {
      std::ifstream in( f ); in >> std::hex;
      unsigned fun , num , dat;
      for( unsigned i = 0 ; i < 1<<(1<<4) ; ++i )
      {
         in >> fun >> num >> dat ; 
         inv[i] = dat ;
         cls[i].resize( num );
         for( unsigned k = 0 ; k < num ; ++ k ){
            in >> dat;
            cls[i][k] = dat ;
         }
      }
   }
   const vector<uint8_t> & operator[]( unsigned idx )const{return cls[idx];}
   unsigned minsop( uint8_t f )const{return inv[f];}
}ecodb(CURDIR"dat/ecodb.dat");
//
//  transformation of the single value
//
inline unsigned encode_hash_doamin( unsigned idx , uint8_t * d ) // for phase 2 , check the valid sim
{
   return (idx<<4)|(d[3]<<3 )|(d[2]<<2)|(d[1]<<1)|d[0] ;
}
inline unsigned encode_hash_codomain( unsigned frame , uint8_t d )
{
   return (frame << 1) | d ;
}
inline char patchar( uint8_t p ){ return (p&2)?'X':(p+'0') ;} // tri-state print 
inline bool diff( uint8_t x , uint8_t y ){ return ((x==0)&&(y==1)) || ((x==1)&&(y==0)) ;} // tri-state compare
inline bool same( uint8_t x , uint8_t y ){ return ((x==0)&&(y==0)) || ((x==1)&&(y==1)) ;} // tri-state compare
static void print_pat( const pat_t & p )
{
   for( unsigned i = 0 ; i < p.size() ; ++ i ) cout << patchar(p[i]); cout << endl;
}
static void print_pat( const pat_t & p , const pat_t & o )
{
   for( unsigned i = 0 ; i < p.size() ; ++ i ) cout << patchar(p[i]); cout << "\t";
   for( unsigned i = 0 ; i < o.size() ; ++ i ) cout << patchar(o[i]); cout << endl;
}
static AigLit trans( AigLit x , AigLit * map )
{
   return map[ var(x) ] ^ sign( x );
}
inline unsigned pat( AigLit x , unsigned * d)
{ 
   return (-sign(x)) ^ d[ var(x)];
}
inline uint8_t pat( AigLit x , uint8_t * d )
{ 
   return sign(x)^d[var(x)] ; 
}
inline unsigned sim( AigNode n , unsigned * d )
{ 
   return pat( n.fanin[0] , d ) & pat( n.fanin[1] , d );
}
inline uint8_t sim( AigNode n , uint8_t * d )
{
#ifdef NO_TRI_STATE
	assert( (pat( n.fanin[0] , d ) & 2) ==0  && (pat( n.fanin[1] , d )& 2) ==0 );
	return pat( n.fanin[0] , d ) & pat( n.fanin[1] , d ) ;
#else
	if( pat( n.fanin[0] , d ) == 0 || pat( n.fanin[1] , d ) == 0 ) return 0;
	if( pat( n.fanin[0] , d ) == 1 && pat( n.fanin[1] , d ) == 1 ) return 1;
	return 2;
#endif
}
static void sim( const StrashAIG & c , const pat_t & p , uint8_t * d )
{
	assert( p[0] == 0 );
   for( unsigned i = 0 ; i < c._andFlag ; ++ i ) 
      d[i] = p[i];
   for( unsigned i = c._andFlag ; i < c.size() ; ++ i )
      d[i] = sim( c[i] , d );
}
static void sim( const StrashAIG & c , const pat_t & p , pat_t & o , unsigned posize,uint8_t * d)
{
	sim( c , p , d );
	assert( o.size() == posize );

	for( unsigned i =  0 ; i < posize ; ++ i ) 
		o[i] = pat( c._po[i] , d );
}
static void trans( const vec<Lit> & a , vec<Lit> & b , GetVar & gv , unsigned f ) // transform to frame f literal 
{
   b.clear(); b.growTo( a.size() );
   for( unsigned i = 0 ; i < a.size() ; ++i) 
      b[i] = Lit( gv( f , a[i].var() ) , a[i].sign() );
}
//
//  circuit createion 
//
inline AigLit createOR( StrashAIG & a , AigLit x , AigLit y )
{
   return inv( a.createAND( inv(x) , inv(y) ) );
}
inline AigLit createXOR( StrashAIG & a , AigLit x , AigLit y )
{
   return createOR( a , a.createAND( x , inv(y) ) , a.createAND( inv(x) , y ) );
}
static void createBase( StrashAIG & ckt , unsigned n ) // create base until n , (the input of pi is n-1)
{
   assert( ckt.size() == 1 );
   for( unsigned i = 0 ; i < n ; ++ i )ckt.createBase(); 
   ckt._andFlag = ckt._ppiFlag = ckt.size();
}
static AigLit create( LUT u , StrashAIG & ckt , AigLit * map  )
{
   unsigned inv = ecodb.minsop( u.init );
   const vector<uint8_t> & buf = ecodb[ inv?((~u.init)&0xFFFF):u.init ];
   
   AigLit x = toAigLit( 0 , 0 );
   for( unsigned i = 0 ; i < buf.size() ; ++ i )
   {
      AigLit y = toAigLit( 0,1 );
      unsigned cube = buf[i];
      for( int j = 0 ; j < 4 ; ++ j , cube = cube>>2 )
      {
         if( (cube&3) == 2 )continue;
         y = ckt.createAND( map[ u[j] ] ^ ((cube&1)^1) , y );
      }

      x = ::inv( ckt.createAND( ::inv( x ) , ::inv( y ) ) );
   }

   return x ^ inv;
}
static AigLit create_sel( LUT u , const AigLit * sel , StrashAIG & ckt , AigLit * map )
{
   AigLit in[4];
   for( unsigned i = 0 ; i < 4 ; ++i ) 
      in[i] = map[ u[i] ];

   AigLit o[16];
   for( unsigned i = 0 ; i < 16 ; ++ i ) 
   {
      AigLit x = ckt.createAND( in[0]^((i)&1)^1 , in[1]^((i>>1)&1)^1 );
      AigLit y = ckt.createAND( in[2]^((i>>2)&1)^1 , in[3]^((i>>3)&1)^1 );
      AigLit z = ckt.createAND( x , y);
      o[i] = ckt.createAND( z , sel[i] );
   }
   for( int i = 3 ; i >= 0 ; -- i )
      for( unsigned j = 0 ; j < (unsigned)(1<<i) ; ++ j )
         o[j] = inv( ckt.createAND( inv( o[(j<<1)] ) , inv( o[(j<<1)|1]  )) );
      
   return o[0];
}
template<class T>
static void topn( T * cost , vector<unsigned> & n , unsigned num , bool zero_care)
{
	if( n.size() <= num )return;

	unsigned size = n.size() ;
	std::pair<T,unsigned> item[ size ];
	for( unsigned i = 0 ; i < size ; ++i ) item[i] = std::make_pair( cost[i] , n[i] );
	std::make_heap( item , item + size );

	n.clear();
	for( unsigned i = 0 ; i < num ; ++ i , -- size  )
	{
		if( zero_care && item[0].first <= 0 )break;
		n.push_back( item[0].second );
		pop_heap ( item , item + size ); 
	}
}
//
//  create Circuits
//
static void create_sorter( StrashAIG & c , unsigned size )
{
   for( unsigned i = 0 ; i < size ; ++ i ) c.createBase();
   c._andFlag = c._ppiFlag = size + 1;
   AigLit n[ size ];
   for( unsigned i = 0 ; i < size ; ++ i ) n[i] = toAigLit( i+1 , 0 );

   for( unsigned i = 0 ; i < size-1 ; ++ i )
   {
      AigLit x = n[0]; 
      for( unsigned j = 1 ; j < size-i  ; ++ j )
      {
         n[j-1] = c.createAND( x , n[j] );
         x = inv( c.createAND( inv(x) , inv(n[j]) ) );
      }
      c._po.push( x );
   }
   c._po.push( n[0] );
}
static void create_copy( const StrashAIG & a , StrashAIG & b , AigLit * map , AigLit * po ) // map is pi literal mapping and buffer use 
{
   for( unsigned i = a._andFlag ; i < a.size() ; ++ i ) 
      map[i] = b.createAND( trans( a[i].fanin[0] , map ) , trans( a[i].fanin[1] , map ) );
   for( unsigned i = 0 ; i < a._po.size() ; ++i )
      po[i] = trans( a._po[i] , map );
}
static void copy( const StrashAIG & a , StrashAIG & b )
{
   for( unsigned i = 1 ; i < a._andFlag ; ++ i ) b.createBase();
   b._andFlag = a._andFlag , b._ppiFlag = a._ppiFlag;
   for( unsigned i = a._andFlag ; i < a.size() ; ++ i )
      b.createAND( a[i].fanin[0] , a[i].fanin[1] );
   for( unsigned i = 0 ; i < a._po.size() ; ++ i )
      b._po.push( a._po[i] );
}
static void external_fraig( StrashAIG & aig , CktCover & cov )
{
#if 0
	aig.write_aig( "bfr.aig" );
	#if 0
		system("bin/synit bfr.aig -o tmp.aig");
		system("bin/fraig tmp.aig afr.aig");
	#else
		system( "echo \'r bfr.aig;ps;dc2; fraig ;w afr.aig;;quit\' | abc > /tmp/nouse.jacky" );
	#endif
	cov.read_aig( "afr.aig" );
#else
	InfoCut x;  copy( aig , x );

	x.init();
	Fraig   fr; synit( x , fr);
	fr.init();
	fr.run();
		
	InfoCut y;
	fr.factor( y );
	y.init();
	
	synit( y, cov );
#endif
}
static void eco_diff( StrashAIG & diff , const StrashAIG & spec , const StrashAIG & design  )
{
   assert( design._andFlag == spec._andFlag && design._po.size() == spec._po.size() );

   createBase( diff , design._andFlag - 1 ); 
   
   unsigned posize = spec._po.size() ;
   AigLit map[ std::max( spec.size() , design.size() ) ] ;
   AigLit spo[ posize ] , rpo[ posize ] , dpo[ posize ] ;
   for( unsigned i = 0 ; i < design._andFlag ; ++i ) 
      map[i] = toAigLit( i , 0 );
   
   create_copy( spec , diff , map , spo );
   create_copy( design , diff , map , rpo );
   
   for( unsigned i = 0 ; i < posize ; ++ i ) 
      dpo[i] =  createXOR( diff , spo[i] , rpo[i] );

	for( unsigned i = 0 ; i < posize ; ++ i )
		diff._po.push( dpo[i] );
}
static void toaig( const FPGA & design , StrashAIG & ckt , AigLit * map )
{
   unsigned andFlag = design.andFlag;

   createBase( ckt , andFlag - 2 );
   assert( ckt._andFlag == andFlag -1 );

   map[0] = toAigLit( 0 , 0 );
   map[1] = toAigLit( 0 , 1 );
   for( unsigned i = 2 ; i < andFlag ; ++ i)
      map[i] = toAigLit( i-1 , 0 );

   for( unsigned i = andFlag ; i < design.size() ; ++ i )
   {
      LUT x = design[i];
      map[i] = create( x , ckt , map );
   }
   for( unsigned i = 0 ; i< design.po.size() ; ++i )
      ckt._po.push( map[ design.po[i] ] ) ;
}
// for 1 candidate there are 16 new input 
static void toselaig( const FPGA & design , StrashAIG & ckt , const vector<unsigned> & cand )
{
   unsigned andFlag = design.andFlag;
   AigLit * map = new AigLit[ design.size() ];
   AigLit * mtpi = new AigLit[ cand.size() << 4 ]; // minterm pi 
   unsigned * iscand = new unsigned[ design.size() ]; 
   memset( iscand , 0xFF , sizeof(unsigned) * design.size() );

   for( unsigned i = 0 ; i < cand.size() ; ++ i) iscand[ cand[i] ] = i;
  
   for( unsigned i = 2 ; i < andFlag ; ++ i )
      map[i] = toAigLit( i-1 , 0 );
   for( unsigned i = 2 ; i < andFlag ; ++ i )
      ckt.createBase();

   unsigned nvar = ckt.size();   
   for( unsigned i = 0 ; i < cand.size() ;++ i )
      for( unsigned j = 0 ; j < 16 ; ++ j )
         mtpi[ (i<<4) | j ] = toAigLit( nvar ++ , 0 ),
         ckt.createBase();

   assert( nvar == ckt.size() );
   ckt._andFlag = ckt._ppiFlag = ckt.size() ;

   map[0] = toAigLit( 0 , 0 );
   map[1] = toAigLit( 0 , 1 );
 
   for( unsigned i = andFlag ; i < design.size() ; ++ i )
   {
      LUT x = design[i];
      if( iscand[i] == 0xFFFFFFFF )
         map[i] = create( x , ckt , map );
      else
         map[i] = create_sel( x , mtpi + (iscand[i]<<4), ckt , map );   
   }
   for( unsigned i = 0 ; i < design.po.size() ; ++i )
      ckt._po.push( map[ design.po[i] ] ) ;

   delete [] map ;delete [] mtpi;delete [] iscand;
}
// 
//  SAT solver 
//
static void addEQCls( Lit o , Lit a , Lit b , MinisatSolver & s ) // can be merge to addXORCls
{
  vec< Lit > v(3);
  v[0] = o , v[1] = a , v[2] = b;   s.addClause( v );
  v[0] = o , v[1] = ~a , v[2] = ~b;   s.addClause( v );
  v[0] = ~o , v[1] = ~a , v[2] = b;   s.addClause( v );
  v[0] = ~o , v[1] = a , v[2] = ~b;   s.addClause( v );
} 
static void add4AND( Lit o , Lit * in , MinisatSolver & s)
{
   vec<Lit> v(5) , w(2);
   v[0] = ~in[0] ,  v[1] = ~in[1] , v[2] = ~in[2] , v[3] = ~in[3] , v[4] = o;
   s.addClause( v );
   w[0] = ~o;
   for( unsigned i = 0 ; i < 4 ; ++i )
   {
      w[1] = in[i] ; 
      s.addClause( w );
   }
}
static void addNEQ( Minisat::Solver & m , Lit a , Lit b )
{
   Minisat::vec< Minisat::Lit > v( 2 ); 
   v[0] = a , v[1] = b;            m.addClause( v );
   v[0] = ~v[0] , v[1] = ~v[1];     m.addClause( v );
}
static void addXORCls( Minisat::Solver & s , Lit o , Lit x , Lit y ) // can be merge with addEQCls 
{
   cls_t v(3);
   v[0] = ~o , v[1] = x , v[2] = y;    s.addClause( v ); // -o  x  y 
   v[1] = ~v[1] , v[2] = ~v[2];        s.addClause( v ); // -o -x -y
   v[0] = ~v[0] , v[1] = ~v[1];        s.addClause( v );//   o x  -y
   v[1] = ~v[1] , v[2] = ~v[2];        s.addClause( v );//   o -x  y
}
static void dump_lut_cnf( unsigned short fun , Lit x[] , vec< vec<Lit> > & cls )
{
   for( unsigned s = 0 ; s < 2 ; ++ s )
   {
      unsigned short idx = (s==0)?fun: (~fun);
      Lit o = s ? (~x[4]) : x[4]; 
      
      const vector<uint8_t> & db = ecodb[idx];
      for( unsigned i = 0 ; i < db.size() ; ++ i )
      {
         uint8_t k = db[i];
         cls.push();
         vec< Lit > & c = cls.last();
         c.push( o );
         for( unsigned j = 0 ; j < 4 ; ++ j , k = k >> 2 )
         {
            if( (k&3) == 2 ) continue; assert( (k & 3) != 3 );
            c.push( x[j] ^ (k&1) );
         }
      }
   }
}
static void dump_mux_cnf( Lit old , Lit rw , Lit s , Lit o , vec< vec<Lit> > & cls )
{
   unsigned idx = cls.size() ;
   cls.growTo( idx + 4 ); 
   for( unsigned i = idx ; i < idx + 4 ; ++ i ) 
      cls[i].growTo( 3 );

   Lit * v;

   v = cls[idx++].data; v[0] = o , v[1] = s , v[2] = ~old ;
   v = cls[idx++].data; v[0] = ~o , v[1] = s , v[2] = old ;
   v = cls[idx++].data; v[0] = o , v[1] = ~s , v[2] = ~rw ;
   v = cls[idx++].data; v[0] = ~o , v[1] = ~s , v[2] = rw ;
}
//
//  Pattern Generation 
//
static bool sim_patg( const StrashAIG & diff , pat_t & p , bool good = false )
{
   p[0] = 0; 

   // try to generate a test pattern such that all the output are come to 1 
   unsigned d[ diff.size() ];
   d[0] = 0;
   unsigned k , cnt = 0 ;

   do
   {
      k = 0x0 , cnt +=1;
      for( unsigned i = 1 ; i < diff._andFlag ; ++ i )
         d[i] = rand();
      for( unsigned i = diff._andFlag ; i < diff.size() ; ++ i )
         d[i] = sim( diff[i] , d );
		for( unsigned i = 0 ; i < diff._po.size() ; ++ i )
			k |= pat( diff._po[i] , d );
		if( good ) k = ~k;

   }while( k == 0 && cnt < (unsigned)Parameter::PAT_SIM_CONF );
   
   if( k == 0 ) return false; 

   // record such pattern to p 
   for( unsigned i = 0 , sign = 1 ; i < 32 ; ++ i , sign = sign << 1 ) 
      if( k & sign )
      {
         for( unsigned j = 1 ; j < diff._andFlag ; ++ j ) 
            p[j] = bool(d[j]&sign);

         break;
      }

   return true;
}
static bool sat_patg( Minisat::Solver & solver , const cls_t & a , Lit * lits , pat_t & p )
{
   p[0] = 0; 
   bool ret = solver.solve( a ); 
   if( ret == false )return false;

   for( unsigned i = 1 ; i < p.size(); ++ i )
      p[i] = solver.modelValue( lits[i].var() ) == Minisat::l_True;
   
   return true;
}
static bool sat_patg_out( MinisatSolver & s , const cls_t & a , CktCover & ckt , pat_t & p , vec<AigLit> & po , vector<bool> & eqpo )
{
	pat_t out( po.size() );

	for( unsigned t = 0 ; t < 100 ; ++ t )
	{
		for( unsigned i = 0 ; i < out.size() ; ++i )
			out[i] = eqpo[i]?0:((rand()%Parameter::P_SEL_SAT_OUT)==0);

		cls_t assumpt;
		for( unsigned i = 0 ; i < out.size() ; ++ i )
			if( out[i] ) assumpt.push( ckt.getLit(po[i]) );
		for( int i = 0 ; i < a.size() ; ++ i ) 
			assumpt.push( a[i] );
		bool ret = s.solve( assumpt );
		if( ret == false ) continue;
		for( unsigned i = 1 ; i < p.size(); ++ i )
			p[i] = s.modelValue( ckt._lits[i].var() ) == Minisat::l_True;
		return true;
	}

	return false;
}
static void add_xor_ckt( StrashAIG & diff , pat_t & p )
{
   AigLit x = toAigLit( 0 , 0 );
   pat_t r = p; for( unsigned i = 0 ; i < p.size() ; ++ i ) r[i] = ((rand()%2)==0);

   for( unsigned i = 1 ; i < diff._andFlag ; ++ i )
      if( r[i] && ((p[i]&2)==0) )
         x = createXOR( diff , x , toAigLit( i , inv(p[i]) ) );

   diff._po.push( x );
}
static Lit add_xor_cls( Minisat::Solver & solver , Lit * lits, pat_t & p)
{
   unsigned var = solver.nVars() , cnt=0 ;
   pat_t r = p; for( unsigned i = 0 ; i < p.size() ; ++ i ) r[i] = ((rand()%2)==0);

   for( unsigned i = 1 ; i < p.size() ; ++ i )
      if( r[i] && ((p[i]&2)==0) ) cnt+=1 ;

   for( unsigned i = 0 ; i < cnt ; ++ i ) 
      solver.newVar();

   Lit x = lits[0];

   for( unsigned i = 1 ; i < p.size() ; ++ i )
      if( r[i] && ((p[i]&2)==0) )
      {
         Lit o = Lit( var ++ , 0 );
         addXORCls( solver , o , x , ( lits[i]^p[i]) );
         x = o;
      }

   assert( (int)var == solver.nVars() );
   return x;
}
static void add_or_cls(  Minisat::Solver & solver , Lit * lits , pat_t & p ) // this is not test yet 
{
	 cls_t cls;
    for( unsigned i = 1 ; i < p.size() ; ++ i )
		 if( (p[i]&2) == 0 )
	       cls.push( lits[i]^p[i] );

    solver.addClause( cls );
}
static unsigned diff_pat( const pat_t & a , const pat_t & b )
{
	unsigned int cnt = 0;
	for( unsigned i = 0 ; i < a.size() ; ++ i )
		if( diff( a[i] , b[i] ) ) cnt+=1;;

	return cnt;
}
static void pattern_min( const StrashAIG & a , const StrashAIG & b , pat_t & p , unsigned posize , vector<unsigned> & ord , uint8_t * bufa , uint8_t * bufb )
{
#ifdef NO_TRI_STATE
	assert( false );
#endif
	std::random_shuffle( ord.begin() , ord.end() );
	pat_t oa(posize), ob(posize);
	
	sim( a , p , oa , posize , bufa );
	sim( b , p , ob , posize , bufb );
	unsigned diffcnt = diff_pat( oa , ob );

	for( unsigned i = 0 ; i < ord.size() ; ++ i )
	{
		p[ ord[i] ] |= 2;
		sim( a , p , oa , posize , bufa);
		sim( b , p , ob , posize , bufb );
		if( diff_pat( oa , ob ) < diffcnt )
			p[ ord[i] ] &= (~2);
	}
}
static void pattern_max_diff( const StrashAIG & a , const StrashAIG & b , pat_t & p , unsigned posize , uint8_t * bufa , uint8_t * bufb )
{
	pat_t oa(posize), ob(posize);
	sim( a , p , oa , posize , bufa );
	sim( b , p , ob , posize , bufb );
	unsigned diffcnt = diff_pat( oa , ob );
	for( unsigned i = 0 ; i < p.size()*10 ; ++ i )
	{
		int idx = rand()%(p.size()-1)+1;
		int reserve = p[ idx ];
		p[idx] = rand()%2 ;
		sim( a , p , oa , posize , bufa);
		sim( b , p , ob , posize , bufb );
		if( diff_pat( oa , ob ) < diffcnt )
			p[ idx ] = reserve;
	}
}
static unsigned gen_pattern_sim_routine( StrashAIG & diff , std::vector< pat_t > & pats )
{
	unsigned andFlag = diff._andFlag;

	vector<unsigned> ord; 
	for( unsigned i = 1 ; i < diff._andFlag ; ++ i ) ord.push_back(i);

	pat_t pat( andFlag );

	while( sim_patg( diff , pat , false ) )
   {
      pats.push_back( pat_t( andFlag ) );
      pats.back().swap( pat );
		if( pats.size() == (unsigned)Parameter::SIM_SIZE )break;
   }

	unsigned psize = pats.size();
	while( sim_patg( diff , pat , true) )
	{
		pats.push_back( pat_t(andFlag ) );
		pats.back().swap( pat );
		if( (pats.size() - psize )== (unsigned)Parameter::SIM_GOOD_SIZE ) break;
	}
   //cout << "sim pat gen " << pats.size() << endl;

	return psize;
}
static unsigned gen_pattern_out_sat_routine( CktCover & ckt , MinisatSolver & s, std::vector< pat_t > & pats , vector<bool> & eqpo )
{
	unsigned andFlag = ckt._andFlag;
	pat_t pat( andFlag );
	
	unsigned psize = pats.size();

	cls_t assumpt;
	while( sat_patg_out( s , assumpt , ckt , pat , ckt._po ,  eqpo ) )
	{
		 add_or_cls( s , ckt._lits , pat );
		//assumpt.push( x );

		pats.push_back( pat_t(andFlag ) );
		pats.back().swap( pat );
		if( (pats.size() - psize )== (unsigned)Parameter::SAT_PAT_OUT_SIZE ) break;
	}
   //cout << "satout pat gen " << pats.size() << endl;
	return pats.size() - psize;
}
static unsigned gen_pattern_sat_routine( CktCover & ckt , std::vector< pat_t > & pats , MinisatSolver & s )
{
	unsigned andFlag = ckt._andFlag;
	pat_t pat( andFlag );

   cls_t assumpt;
	{
		unsigned posize = ckt._po.size();
		vec<Lit> outor( posize );
		for( unsigned i = 0 ; i < posize ; ++ i )
			outor[i] = ckt.getLit( ckt._po[i] );
		s.addClause( outor );
	}
	unsigned psize = pats.size();

   while( sat_patg(  s , assumpt , ckt._lits , pat ) && s.conflicts < (unsigned)Parameter::PAT_SAT_CONF )
   {
      Lit x = add_xor_cls( s , ckt._lits , pat );
      assumpt.push( x );
      pats.push_back( pat_t( andFlag ) );
      pats.back().swap( pat );
	}
   //cout << "sat pat gen "<< pats.size() << endl;
	return pats.size() - psize ;
}
bool gen_pattern( const StrashAIG & spec , const StrashAIG & design , vector< pat_t > & pati , vector<bool> & eqpo )
{
   StrashAIG tmp;
   CktCover  diff;

   eco_diff( tmp , spec , design );
  	external_fraig( tmp , diff );

	{ // collect eqpo , and counting is the output is sat
		unsigned eqcnt=0;
		eqpo.clear(); eqpo.resize( diff._po.size() , 0 ) ;
		for( unsigned i = 0 ; i < diff._po.size() ; ++ i )
			if( diff._po[i] == 0 ) 
				 eqpo[i] = 1 , eqcnt +=1 ;
		if( eqcnt == design._po.size() ) return false;
	}

   unsigned diffsize = gen_pattern_sim_routine( diff , pati );

	MinisatSolver s;
	diff.init( 0 ) , diff.covering() , diff.assignLit( 0 );
   for( unsigned i = 0 ; i < diff.nVars() ; ++ i )s.newVar();
   diff.assignCNF( s );

	gen_pattern_out_sat_routine( diff , s  , pati , eqpo );
	if( diffsize < (unsigned)Parameter::SIM_SIZE )
   	gen_pattern_sat_routine( diff , pati , s);

	return true;
}
//
//  Candidate Generation
//
static double propagate( double c , uint8_t v , LUT x ,uint8_t * d , double * sc )
{
	if( v&2 ) return 0;
	const double ci = Parameter::PUSH_TO_INPUT_FACTOR;

   unsigned short idx = (v==0) ? x.init : ~x.init; 
	double minpos=c;
	c /=  ecodb[idx].size() ;
	unsigned size =0 ;
	for( unsigned j = 0 ; j < 4 ; ++ j ) 
		if( x[j]!=0 && ((d[x[j]]&2)!=0)) size+=1;

   for( unsigned i = 0 ; i < ecodb[idx].size() ; ++ i )
   {
      uint8_t k = ecodb[idx][i];
      unsigned cnt = 0 ;

      for( unsigned j = 0 ; j < 4 ; ++j , k = k >> 2 )
      {
			if( x[j] == 0 || (d[x[j]]&2) || (k&3) == 2 ) continue;
         if( (k&3)^d[ x[j] ] )
            cnt +=1;
      }
      k = ecodb[idx][i];
      for( unsigned j = 0 ; j < 4 ; ++ j , k = k >> 2 )
      {
			if( x[j] == 0 || (d[x[j]]&2) || (k&3) == 2 ) continue;
         
			if( (k&3)^d[ x[j] ] && cnt != 0 )
			{
            sc[ x[j] ] += (ci*c)/cnt;
				if( minpos > 0 ) minpos = std::min( minpos , c/cnt );
			}
			else if( (size-cnt) != 0 )
			{
				sc[ x[j] ] -= (ci*c)/(size-cnt);
				if( minpos < 0 ) minpos = std::max( minpos , c/(size-cnt) );
			}
      }
   }

	return minpos;
}
static void pat_base_candidate( const StrashAIG & spec , FPGA & design , const vector< pat_t > & pats , vector< pat_t > & gout ,double * score )
{
   uint8_t * pat0 = new uint8_t [ spec.size() ];
   uint8_t * pat1 = new uint8_t [ design.aig->size() ];
   uint8_t * pat2 = new uint8_t [ design.size() ];
   double  * sc   = new double  [ design.size() ];
	unsigned * diffcnt = new unsigned[ design.po.size() ];
	unsigned * eqcnt   = new unsigned[ design.po.size() ];

	// compute diffcnt 
	memset( diffcnt , 0 , sizeof(unsigned)*design.po.size() );
	memset( eqcnt , 0 , sizeof(unsigned)*design.po.size() );

	for( unsigned k = 0 ; k < pats.size() ; ++ k )
	{
		sim( spec , pats[k] , pat0 );
		sim( *design.aig , pats[k] , pat1 );
		for( unsigned i = 0 ; i < design.po.size() ; ++ i )
		{
			if( diff( pat( spec._po[i] , pat0 ) , pat( design.aig->_po[i] , pat1 ) ) )
				diffcnt[i] +=1 ;
			if( same( pat( spec._po[i] , pat0 ) , pat( design.aig->_po[i] , pat1 ) ) )
				eqcnt[i] += 1;
		}
	}

   for( unsigned k = 0 ; k < pats.size() ; ++ k )
   {
      for( unsigned j = 0 ; j < design.size() ; ++ j ) sc[j] = 0;
      
      // sim the pattern 
      sim( spec , pats[k] , pat0 );
      sim( *design.aig , pats[k] , pat1 );
      for( unsigned i = 0 ; i < design.size() ; ++ i )
         pat2[i] = pat( design.mapping[i] , pat1 );
      for( unsigned i = 0 ; i < design.po.size() ; ++ i )
         gout[k][i] = pat0[ var(spec._po[i]) ] ^ sign( spec._po[i] );

      // setting out 
      for( unsigned i = 0 ; i < spec._po.size() ; ++ i ) 
		{
			if( diff( pat( spec._po[i] , pat0 ) , pat( design.aig->_po[i] , pat1 ) ) )
            sc[ design.po[i] ] = 200.0/diffcnt[i];
			if( same( pat( spec._po[i] , pat0 ) , pat( design.aig->_po[i] , pat1 ) ) )
				sc[ design.po[i] ] = -100.0/eqcnt[i];
		}

      for( unsigned i = design.size() -1 ; i>= design.andFlag ; -- i )
		{
         sc[i] -= Parameter::PUSH_TO_OUTPUT_FACTOR*propagate( sc[i] , pat2[i] , design[i] , pat2 ,  sc );
			sc[i] /= sqrt( design.focnt[i] );			
		}

      for( unsigned i = 0 ; i < design.size() ; ++i ) 
			score[i] += sc[i];
		design.record_score( sc , k );
   }
   delete [] pat0 ;delete [] pat1 ; delete [] pat2 ; delete [] sc; delete [] diffcnt; delete [] eqcnt;
}
// setting the non traversed no to invalid 
static void filter( const FPGA & design , double * score , const vector<bool> & eqpo )
{
	bool * innocent = new bool[ design.size() ];
	double * factor = new double[ design.size() ];

	vector<unsigned> v;
	unsigned ptr=0;

	for( unsigned i = 0 ; i < eqpo.size() ; ++ i )
		if( eqpo[i] ){
			memset( innocent , 0 , sizeof(bool)*design.size()  );

			if( innocent[ design.po[i] ] == 0 && design.po[i] >= design.andFlag ){
				v.clear(); ptr=0;
				innocent[ design.po[i] ] = 1;
				v.push_back( design.po[i]) ;
				factor[ design.po[i] ] = Parameter::FILTER_FACTOR;

				while( ptr != v.size() ){ 
					double f = factor[ v[ptr] ];
					LUT x = design[ v[ptr++ ] ];

					for( int j = 0 ; j < 4 ; ++ j ){
						if( innocent[ x[j] ] == 0 && x[j] >= design.andFlag ){
							innocent[ x[j] ] = 1 ;
							score[ x[j] ] /= f;
							factor[ x[j]] = f*0.9;
							v.push_back( x[j] );
						}
					}
				}
			}
		}

	delete [] innocent; delete [] factor;
}
void get_candidate( vector<unsigned> & cand , FPGA & design , const StrashAIG & spec , const vector< pat_t > & pats , vector<pat_t> & gout , const vector<bool> & eqpo )
{
   // using the pattern to commpute the score
   double * score = new double [ design.size() ]; 
   for( unsigned i = 0 ; i < design.size() ; ++ i) score[i] = 0;

   pat_base_candidate( spec , design , pats , gout , score );
	filter( design , score , eqpo );

   double max=0;
   for( unsigned i = design.andFlag ; i < design.size() ; ++ i ) 
		if( score[i] > max ) 
			max = score[i];
   double threadhold = max / Parameter::CAND_SCORE;
   // marking the candidate 
   for( unsigned i = design.andFlag ; i < design.size() ; ++ i )
      if( score[i] > threadhold )
         cand.push_back( i ) ;
	
	if( cand.size() > (unsigned)Parameter::CAND_UBOUND || cand.size() < (unsigned)Parameter::CAND_LBOUND )
	{
		unsigned candsize=0;
		if( cand.size() > (unsigned)Parameter::CAND_UBOUND ) candsize = Parameter::CAND_UBOUND;
		if( cand.size() < (unsigned)Parameter::CAND_LBOUND ) candsize = Parameter::CAND_LBOUND;

		if( cand.size() < (unsigned)Parameter::CAND_LBOUND )
		{
			cand.clear();
			for( unsigned i = design.andFlag ; i < design.size() ; ++ i ) 
				cand.push_back( i );
		}

		double cscore[ cand.size() ];
		for( unsigned i = 0 ; i < cand.size() ; ++ i ) cscore[i] = score[ cand[i] ];

		topn( cscore , cand , candsize , false ); // don't care less than 0 
	}

   delete [] score;
}
//
//  SAT Refine Candidate 1 , assign the constraint 
//
static unsigned dump_eco_cnf( const vector<unsigned> & candidate , const FPGA & design , MuxCktLit & lit, vec< vec<Lit> > & clses )
{
   Lit * sel = lit.selection , * rw = lit.rewire , * lits = lit.lits; 
   
	unsigned var = 0;
   unsigned * cand = new unsigned[ design.size() ]; 

   memset( cand , 0xFF ,  sizeof(unsigned)*design.size() );
   for( unsigned i = 0 ; i < candidate.size() ; ++ i )
      cand[ candidate[i] ] = i ;
   Lit tmpo[ candidate.size() ];
   
   // assign Literal 
   for( unsigned i = 0 ; i < candidate.size() ; ++ i) 
      sel[i] = Lit( var++,0);
   
   for( unsigned i = 0 ; i < design.size() ; ++ i ) 
      lits[i] = Lit( var++,0);

   for( unsigned i = 0 ; i < candidate.size() ; ++ i )
      tmpo[i] = Lit( var++,0);

   for( unsigned i = 0 ; i < candidate.size() ; ++ i )
      rw[i] = Lit(var++,0);

   // assign clause , const and the 
   for( unsigned i = design.andFlag ; i < design.size() ; ++i )
   {
      Lit x[5];
      LUT L = design[i];
      for( unsigned j = 0 ; j < 4 ; ++ j ) x[j] = lits[ L[j] ];
      x[4] = ((cand[i])==0xFFFFFFFF) ? lits[i] : tmpo[ cand[i] ] ;
      dump_lut_cnf( L.init , x , clses );
      if( cand[i] != 0xFFFFFFFF )
         dump_mux_cnf( tmpo[ cand[i] ] , rw[ cand[i] ] , sel[ cand[i] ] , lits[i] , clses );
   }
   {
      clses.push(); clses.last().push( ~ lits[0] );
      clses.push(); clses.last().push(  lits[1] );
   }
	delete [] cand;
   return var ;
}
static void dump_cnf( MinisatSolver & s , unsigned ps , GetVar & gv , vec< vec<Lit> > & clses)
{
   unsigned nv = gv._diff * ps +  gv._base; 
   for( unsigned i = 0 ; i < nv ;++ i ) s.newVar();
   
   vec<Lit> v;
   for( unsigned i = 0 ; i < ps ; ++ i )
      for( unsigned j = 0 ; j < clses.size() ; ++ j )   
      {
         trans( clses[j] , v , gv , i );
         s.addClause( v );
      }
}
static void assign_pats( const vector< pat_t > & pati , const vector<pat_t> & pato , MinisatSolver & s , const vector<unsigned> & po, Lit * lits , GetVar & gv )
{
   vec<Lit> v(1);
   for( unsigned i = 0 ; i < pati.size() ; ++i )
   {
      for( unsigned j = 1 ; j < pati[i].size() ; ++ j )
      {
			if( pati[i][j] & 2 ) continue;
         v[0] = gv( i , lits[j+1] ) ^ pati[i][j] ^ 1 ;
         s.addClause( v );
      }
      for( unsigned j = 0 ; j < pato[i].size() ; ++ j ) 
      {
			if( pato[i][j] & 2 ) continue;
         v[0] = gv( i , lits[ po[j] ] ) ^ pato[i][j] ^ 1 ;
         s.addClause( v );
      }
   }
}
static void create_sorter( Lit * in, Minisat::vec< Minisat::Lit > & assumpt, unsigned size , MinisatSolver & s )
{
   CktCover sorter;
   create_sorter( sorter , size );
   sorter.init( 0 );
   sorter.covering();

   unsigned nvar = s.nVars();
   for( unsigned i = 0 ; i < size ; ++ i )
      sorter._lits[i+1] = in[i];
   sorter.assignLit( nvar );
   while( (unsigned)(s.nVars()) != sorter.nVars() ) 
      s.newVar();
   assumpt.growTo( size );
   for( unsigned i = 0 ; i < size ; ++ i )
      assumpt[i]  = ~sorter.getLit( sorter._po[i] );

   sorter.assignCNF( s );
}
//
//  SAT Refine Candidate 2 , iteratively solve min selection 
//
static void valid_solve( const vector<unsigned> & cand , unsigned fsize , MuxCktLit & ml , GetVar & gv, const FPGA & design , MinisatSolver & s , vector<Triple> & conf )
{
   Lit * lits = ml.lits , * rw = ml.rewire , * sel = ml.selection;

   std::tr1::unordered_map< unsigned , unsigned > hash;
   uint8_t d[5];
   for( unsigned f = 0 ; f < fsize ; ++ f )
   {
      for( unsigned c = 0 ; c < cand.size() ; ++ c ) 
      {
         if( s.modelValue( sel[ c ] ) != l_True ) continue;
         
         // get the value of rewire and the value of the input 
         unsigned idx = cand[c];
         LUT lut = design[idx];
         for( unsigned i = 0 ; i < 4 ; ++ i )
            d[i] = ( s.modelValue( gv( f , lits[ lut[i] ] ) ) == l_True );
         d[4] = (s.modelValue( gv( f , rw[c] ) ) == l_True );
         // insert the idx/value to frame/value pair
         
         unsigned x = encode_hash_doamin( c , d );
         unsigned y = encode_hash_codomain( f , d[4] );
         if( hash.find(x) != hash.end() )
         {
            unsigned y2 = hash.find(x)->second ;
            if( (y2^y)&1 ) 
               conf.push_back( Triple(x>>4 , y >> 1 , y2 >> 1) );
         }
         else hash.insert( std::make_pair( x , y ) ) ;
      }
   }
}
static void add_lut_eq_constraint( Lit * x , Lit * y , Lit a , Lit b , unsigned & nvar , MinisatSolver & s )
{
   // create the big eq and a and 
   Lit tmp[4];
   for( unsigned i = 0 ; i < 4 ; ++ i) 
   {
      tmp[i] = Lit( nvar ++ , 0 );
      addEQCls( tmp[i] , x[i] , y[i] , s );
   }
   Lit out = Lit( nvar ++ , 0 );
   add4AND( out , tmp , s );
   // add
   vec<Lit> v(3);
   v[0] = ~out , v[1] = a , v[2] = ~b;
   s.addClause( v );
   v[0] = ~out , v[1] = ~a , v[2] = b;
   s.addClause( v );
}
static void add_lut_eq_constraint( vector<Triple> & conf , const vector<unsigned> & cand , MuxCktLit & ml , GetVar gv , const FPGA & design , MinisatSolver & s )
{
   Lit * lits = ml.lits , * rw = ml.rewire ;
   unsigned nvar = s.nVars();
   for( unsigned i = 0 ; i < conf.size() * 5 ; ++ i ) s.newVar();

   for( unsigned i = 0 ; i < conf.size() ; ++i )
   {
      Lit x[4] , y[4] , a , b ;
      // getting the literal , and add the xor constraint 
      unsigned idx = conf[i].dat[0] , f0 = conf[i].dat[1] ,f1 = conf[i].dat[2];
      a = gv( f0 , rw[idx] ); // get the rewire signal at frame 
      b = gv( f1 , rw[idx] );

      LUT lut = design[ cand[idx] ];
      for( unsigned j = 0 ; j < 4 ; ++ j ) 
         x[j] = gv( f0 , lits[ lut[j] ] ),
         y[j] = gv( f1 , lits[ lut[j] ] );
      add_lut_eq_constraint( x , y , a , b , nvar , s );
   }
   assert( nvar == (unsigned)(s.nVars()) );
}
static bool refine_candidate( const vector<unsigned> & cand , unsigned * candcnt , MinisatSolver & s , MuxCktLit & lits , const FPGA & design , const cls_t & assumpt , unsigned nsel , unsigned psize , GetVar & getvar )
{
	// clear assumption 
	cls_t a; assumpt.copyTo(a);
	unsigned selidx = 0;
	while( 1 )
	{
		bool ret = s.solve( a ); 
		if( ret == false )
		{
			if( selidx == nsel ){ return false ;}
			a[ selidx ] = ~a[ selidx ];
			selidx +=1 ; continue;
		}
		vector<Triple> conf;
		valid_solve( cand , psize , lits , getvar , design , s , conf );
		if( conf.size() == 0 ) break;
		add_lut_eq_constraint( conf , cand , lits , getvar , design , s );
	};
	for( unsigned i = 0 ; i < cand.size() ; ++ i )
		if( s.modelValue( lits.selection[i] ) == l_True )
			candcnt[ i ] +=1 ;

	return true ;
}
bool refine_candidate( vector<unsigned> & cand , const FPGA & design , const vector< pat_t > & pati , const vector< pat_t > & pato )
{
   MuxCktLit lits( cand.size() , design.size() );
   MinisatSolver s;
   Minisat::vec< Minisat::Lit > assumpt;
   GetVar getvar;
   {
      vec< vec<Lit> > clses;  
      unsigned nvar = dump_eco_cnf( cand , design, lits , clses );
   
      getvar.init( cand.size() , nvar );
      dump_cnf( s , pati.size() , getvar , clses );   
      assign_pats( pati , pato , s , design.po , lits.lits , getvar );
      create_sorter( lits.selection , assumpt , cand.size() , s );
   }
	unsigned nsel = assumpt.size();
	unsigned candcnt[ cand.size() ]; memset( candcnt , 0 , sizeof(unsigned)*cand.size() );

	bool ret = refine_candidate( cand , candcnt , s , lits , design , assumpt , nsel , pati.size() , getvar );
	if( ret == false ) return false;
	
	vector<unsigned> rcandidx;
	for( unsigned i = 0 ; i < cand.size() ; ++ i ) if( candcnt[i] ) rcandidx.push_back(i);
	for( unsigned i = 0 ; i < rcandidx.size() ; ++ i )
	{
		assumpt.push( ~ lits.selection[ rcandidx[i] ] );
		bool ok = refine_candidate( cand , candcnt , s , lits , design , assumpt , (unsigned)(rcandidx.size()*Parameter::REFINE_FACTOR1)  , pati.size() , getvar );
		if( ok == false ) candcnt[ rcandidx[i] ] += rcandidx.size() ;
		assumpt.pop();
	}

	topn( candcnt , cand , (unsigned)(rcandidx.size()*Parameter::REFINE_FACTOR2) , true);

	return ret;
}
//
//  synthesis result return out literal
//
static unsigned createConstCkt( const StrashAIG & ckt , const pat_t & p , StrashAIG & o )
{
	assert(p[0]==0);
   assert( ((ckt._andFlag - p.size()) & 0xF ) == 0 );
   AigLit m[ ckt.size() ];
	unsigned bcnt=1;
	for( unsigned i = 0 ; i < p.size() ; ++ i ){
		if( p[i] & 2 )
		{ 
			m[i] = toAigLit( bcnt++ , 0 ) ;
			o.createBase() ;
		}
		else 
			m[i] = toAigLit(0,p[i]);
	}

	for( unsigned i=p.size() , j = bcnt ; i < ckt._andFlag ; ++ i , ++j)
		m[i] = toAigLit( j ,0), o.createBase();

   o._andFlag = o._ppiFlag = o.size();
   for( unsigned i = ckt._andFlag ; i < ckt.size() ; ++ i )
   {
      AigNode n = ckt[i];
      m[i] = o.createAND( trans( n.fanin[0] , m ) , trans( n.fanin[1] , m ) );
   }
   for( unsigned i = 0 ; i < ckt._po.size() ; ++ i )
      o._po.push( trans( ckt._po[i] , m ) );
	return bcnt;
}
static void addCosntraint( MinisatSolver & s , const StrashAIG & selaig , Lit * mtpi , const pat_t & pati , const pat_t & pato  )
{
   CktCover cov;
   unsigned bcnt = createConstCkt( selaig , pati , cov );
   cov.init( 0 );
   cov.covering();
   for( unsigned i = pati.size() ,k=0 , j = bcnt ; i < selaig._andFlag ; ++ i , ++j , ++k )
      cov._lits[ j ] = mtpi[ k ];

   cov.assignLit( s.nVars() );
   while( (unsigned)(s.nVars()) != cov.nVars() ) s.newVar();

   cov.assignCNF( s );
   vec< Lit > v(1);
   for( unsigned i = 0 ;i < cov._po.size() ; ++ i )
   {
		if( pato[i] & 2 ) continue;
      v[0] = cov.getLit( cov._po[i] ) ^ pato[i] ^ 1; 
      s.addClause( v );
   }
}
static void get_model( MinisatSolver & s , cls_t & v )
{
   for( unsigned i = 0 ; i < (unsigned)(v.size()) ; ++ i )
      v[i] = Minisat::mkLit( var( v[i] ) , s.modelValue( var( v[i] ) ) == l_False );
}
static void get_model( MinisatSolver & s , Lit * in , pat_t & pat) 
{
   pat[0] = 0;
   for( unsigned i = 0 ; i < pat.size() ; ++ i )
      pat[i] = (s.modelValue( in[i] ) == l_True);
}
// add v , slit until 1 , pilit to assumpt
static void get_assumpt_cls( const cls_t & v , MinisatSolver & s , const cls_t & slit ,  pat_t witness , Lit * pilit, cls_t & assumpt )
{
	assumpt.clear();

	for( int i = 0 ; i < v.size() ; ++ i ) 
		assumpt.push( v[i] );

	int k=0;
	for( k=0 ; k < slit.size() ; ++ k ) 
		if( s.modelValue( slit[k] ) == l_False ) 
			break;
	assert( k );
	assumpt.push( ~slit[k-1] );

	for( unsigned i = 1 ; i < witness.size() ; ++ i ) 
		assumpt.push( pilit[i] ^ witness[i]^1 );
}
static void tomiterselaig( const StrashAIG & selaig , const StrashAIG & spec , CktCover & ckt , vector<bool> eqpo )
{
	StrashAIG miter;
	unsigned osize = spec._po.size();
	
	unsigned cnt = 0; 
	for( unsigned i = 0 ; i < eqpo.size() ; ++ i ) cnt += (eqpo[i]==0);

	copy( selaig , miter );
	AigLit m[ spec.size() ];
	for( unsigned i = 0 ; i < spec._andFlag ; ++ i ) 
		m[i] = toAigLit(i,0);
	for( unsigned i = spec._andFlag ; i < spec.size() ; ++ i ) 
	{
		AigNode n = spec[i];
		m[i] = miter.createAND( trans( n.fanin[0] , m ) , trans( n.fanin[1] , m ) );
	}
	for( unsigned i = 0 ; i < spec._po.size() ; ++ i ) 
		miter._po.push( trans( spec._po[i] , m ) );
	for( unsigned i = 0 ; i < osize ; ++ i )
		miter._po[i] = createXOR( miter , miter._po[i] , miter._po[i+osize] );
	miter._po.sz = osize;

	external_fraig( miter , ckt );
}
static void tosolver( CktCover & ckt , MinisatSolver & s1 , MinisatSolver & s2 , unsigned andFlag , unsigned osize , Lit * mtpi , Lit * pilit , Lit * polit)
{
	ckt.init( 0 );
	ckt.covering();
	for( unsigned i = andFlag , j = 0 ; i < ckt._andFlag ; ++ i , ++ j )
		ckt._lits[i] = mtpi[j];
	ckt.assignLit( s1.nVars() );
	for( unsigned i = 0 ; i < andFlag ; ++ i ) 
		pilit[i] = ckt._lits[i];
	for( unsigned i = 0 ; i < osize ; ++ i )
		polit[i] = ckt.getLit( ckt._po[i] );

	assert( s1.nVars() == s2.nVars() );
	while( (unsigned)(s1.nVars()) != ckt.nVars() ) s1.newVar() , s2.newVar();
	ckt.assignCNF( s1 );
	ckt.assignCNF( s2 );
}
static void min_assumpt( MinisatSolver & s , Minisat::vec< Minisat::Lit > & cls , int flag)
{
	cls.clear();
	for( int i = 0 ; i < s.conflict.size(); ++ i )
		if( var( s.conflict[i] ) < flag ) 
			cls.push( s.conflict[i] );
}
unsigned synthesis_selection( cls_t & v , const vector<unsigned> & cand , const FPGA & design , const StrashAIG & spec , const vector<pat_t> & pati , vector<pat_t> & pato , const vector<bool> & eqpo , unsigned pfcore , vector<pat_t> & learn )
{
	assert( v.size() == ((int)(cand.size() << 4)) );
	
   MinisatSolver S1 , S2;
  	cls_t blkcls , eqcls ; // eqlit is same at S1 and S2  

   pat_t witness( spec._andFlag ) , witnessout( spec._po.size() );;
   uint8_t buf[spec.size()];
	for( unsigned i = pato.size() ; i < pati.size() ; ++i )
	{
		sim( spec , pati[i] , witnessout , spec._po.size() , buf );
		pato.push_back( pat_t( spec._po.size() ) ) ;
		pato.back().swap( witnessout );
	}

	// init the minterm literal 
	Lit mtpi[ cand.size() << 4 ] , pilit[spec._andFlag] , polit[ spec._po.size() ];
	for( int i = 0 ; i < v.size() ; ++ i )
		v[i] = mtpi[i] = Lit( i , 0 ) , S1.newVar() , S2.newVar();
	unsigned cubelitflag = S1.nVars(); assert( cubelitflag == (cand.size() << 4 ) );

   StrashAIG sel;
	CktCover  miter;

	// transfer circuit to circuit and solver 
   toselaig( design , sel , cand );
	tomiterselaig( sel , spec , miter , eqpo );
	tosolver( miter , S1 , S2 , spec._andFlag , spec._po.size() , mtpi , pilit , polit );

	// collect the literal 
	for( unsigned i = 0 ; i < eqpo.size() ; ++ i )
		eqcls.push( ~miter.getLit(miter._po[i]) ),
		blkcls.push( miter.getLit(miter._po[i]) );
	Lit ctrl = Lit( S1.nVars() , 0 ); S1.newVar() , blkcls.push( ~ctrl );
	((Minisat::Solver&)S1).addClause( blkcls );

	if( pfcore == false ) 
	   for( unsigned i = 0 ; i < pati.size() ; ++ i ) 
	      addCosntraint( S2 , sel , mtpi , pati[i] , pato[i] );

   unsigned nsol=0;
	unsigned diff=0;
   while( 1 )
   {
      nsol +=1;
      bool ret = S2.solve( eqcls ); // return the model
      if( ret == false ){ diff = 1 ; break;}

      get_model( S2 , v );v.push( ctrl );
		ret = S1.solve( v );v.pop();
		if( ret == false ){ diff = 0; break; }
		
		get_model( S1 , pilit , witness );
		learn.push_back( witness );

		if( pfcore == 0 )
		{
			sim( spec , witness , witnessout , spec._po.size() , buf );
			addCosntraint( S2 , sel , mtpi , witness , witnessout );
		}else
		{
			cls_t assumpt;
			if( pfcore == 1 )
			{
				v.copyTo( assumpt );
				for( unsigned i = 1 ; i < witness.size() ; ++ i ) assumpt.push( pilit[i] ^ witness[i] ^ 1 );
				for( int i = 0 ; i < eqcls.size() ; ++ i ) assumpt.push( eqcls[i] );
	
				ret = S1.solve( assumpt ); assert( ret == false );
				min_assumpt( S1 , assumpt , cubelitflag);
			}else // pfcore == 2
				for( int i = 0 ; i < v.size() ; ++ i ) assumpt.push( ~v[i] );
			((Minisat::Solver&)S2).addClause( assumpt );
		}
   }

   cout << "synthesis solve #"<< nsol <<"\t" ;
	return diff;
}
void revise( FPGA & design , vector<unsigned> & cand , Minisat::vec< Minisat::Lit > & v)
{
   for( unsigned i = 0 ; i < cand.size() ; ++ i )
   {
      unsigned idx = cand[i];
      unsigned init =0;
      for( unsigned j = 0 , s = 1 ; j < 16 ; ++ j , s = s << 1 )
         if( sign( v[ (i<<4) | j ] ) == 0 )
            init |= s;
      design[ idx ].init = init ;   
   }
	delete design.aig;
	design.aig = new StrashAIG();
	toaig( design , * design.aig , design.mapping );
}

void FPGA::init()
{
   mapping = new AigLit[ size() ];
	aig = new StrashAIG();
   toaig( *this , * aig , mapping );
	
	focnt = new unsigned[size()];
	level = new unsigned[size()];
	// compute level
	for( unsigned i = 0 ; i < andFlag ; ++ i ) level[i] = 1 ;
	for( unsigned i = andFlag ; i < size() ; ++ i ){
		unsigned maxlvl=0;
		for(unsigned j=0;j<4;++j)
			if( level[at(i)[j]] > maxlvl ) maxlvl = level[at(i)[j]];
		level[i] = maxlvl+1;
	}
	// compute focnt 
	memset( focnt , 0 , sizeof(unsigned)*size() );
	for( unsigned i = 0 ; i < po.size() ; ++ i )
		focnt[ po[i] ] += 2;
	for( unsigned i = andFlag ; i < size() ; ++ i) 
		for( unsigned j=0;j<4;++j)
			focnt[at(i)[j]] +=1;
}
void FPGA::report()
{
   cout << "FPGA " << andFlag-2 << " " <<size() - andFlag <<  " "  << po.size() << endl;
}
void FPGA::init_plot( unsigned vs )
{
	unsigned s = size(); 
	plot_score = new double * [s];
	for( unsigned i = 0 ; i < s ; ++ i )
	{
		plot_score[i] = new double[vs];
		for( unsigned j = 0 ; j < vs ; ++ j ) 
			plot_score[i][j] = 0;
	}
}
void FPGA::plot( const char * file , unsigned vs , vector<unsigned> & cand , vector<unsigned> & ans )
{
	std::ofstream out(file);
	out << std::fixed ;
	out.precision(2);
	out << "digraph{" << std::endl;
	for( unsigned i = 0 ; i < size() ; ++ i )
	{
		out << "_" << i <<"[shape=box,label=\"";
		double tot=0;
		for( unsigned j = 0 ; j < vs ; ++ j )
		{
			tot += plot_score[i][j];
			out << plot_score[i][j] << "   " ;
			if( (j%4) ==0 ) out << "\\n";
		}
		out << "\\ntot= "<< tot << "\\nidx = " << i  ;
		out << "\"];" << std::endl;
	}
	

	for( unsigned i = andFlag ; i < size() ; ++ i )
		for( unsigned j = 0 ; j < 4 ; ++ j )
			if( at(i)[j] != 0 ) 
				out << "_" << at(i)[j] << " -> _" << i <<";"<< endl;
	for( unsigned i = 0 ; i < po.size() ; ++ i )
		out << "_" << po[i] << "[fontcolor=blue];";
	for( unsigned i = 0 ; i < cand.size() ; ++ i )
		out << "_" << cand[i] << "[color=red];";
	for( unsigned i = 0 ; i < ans.size() ; ++ i )
		out << "_" << ans[i] << "[fillcolor=gray,style=filled];" ;
	out << "}" << std::endl;
}
